package utils;

import java.util.Set;
import java.util.TreeSet;

import kb.DescriptionLogicsKB;

import reasoner.KBReason;
import utils.parser.*;
import utils.exception.CoreReasoningException;
import utils.exception.SyntaxParsingException;
import entities.assertion.Assertion;
import entities.concept.AndConcept;
import entities.concept.Concept;
import entities.concept.ExistsConcept;
import entities.role.GeneralRolePath;
import entities.role.Role;

public class Util {

	private static Set<String> listOfConstantsInTbox = new TreeSet<String>();
	private static String[] listOfConstantsArray;
	private static int oldSize = 0;
	private static final KBReason reasoner = new KBReason(false);
	private static int counter = 0;

	public static KBReason getReasoner() {
		return reasoner;
	}

	public static int getCounter() {
		return counter;
	}

	public static void addKBConstants(String s) {
		listOfConstantsInTbox.add(s);
	}

	// test if K |= C-> D iff K |= a:(~ C or D) is unsat
	// public static boolean subsumes(Concept a, Concept b, TBox tb){
	// // System.out.print("Computing: " + a + " [under] " + b + " => ");
	// Concept c = new NotConcept(a);
	// Concept consist = new OrConcept(b, c);
	// // Completion comp = new Completion(consist, tb);
	// // boolean res = !comp.isSatisfiable();
	// boolean res = reasoner.subsumes(consist, tb);
	// counter += 1;
	// // System.out.println(res);
	// return res;
	// }

	// test if T |= a under b, as T and i:a |= i:b

	public static boolean subsumes(Concept lhs, Concept rhs,
			DescriptionLogicsKB kb) {
		KBReason res = new KBReason(false);
		try {
			return res.subsumes(lhs, rhs, kb);
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
		return false;
	}

	public static boolean assertionCheck(Assertion lhs, Assertion rhs,
			DescriptionLogicsKB kb) {
		KBReason res = new KBReason(false);
		try {
			return res.logicConsequence(lhs, rhs, kb);
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
		return false;
	}

	public static Concept parseConcept(String s, DescriptionLogicsKB kb) {
		Concept c = null;
		try {
			c = Parser.conParser(Parser.getListOfTokensFromTokenizer(s), kb);
		} catch (SyntaxParsingException e) {
			e.printStackTrace();
		}
		// Tokenizer t = new Tokenizer(s);
		// LinkedList<String> list = new LinkedList<String>();
		// while(t.hasNextToken()) {
		// String st = null;
		// try {
		// st = t.nextToken();
		// } catch (IOException e) {
		// e.printStackTrace();
		// }
		// list.add(st);
		// }
		// Concept c = null;
		// try {
		// c = Parser.conParser(list, null);
		// } catch (SyntaxParsingException e) {
		// e.printStackTrace();
		// }
		//
		return c;
	}

	public static Set<String> getListOfConstantsInTbox() {
		return listOfConstantsInTbox;
	}

	public static Concept parseConceptFromGeneralRolePath(GeneralRolePath grp,
			Concept c) {
		if (grp == null || grp.length() == 0) {
			return c;
		}
		Concept rc = c;
		for (int i = grp.length() - 1; i >= 0; i--) {
			Object item = grp.getContent().get(i);
			if (item instanceof Role) {
				rc = new ExistsConcept((Role) item, rc);
			} else if (item instanceof Concept) {
				rc = ((Concept) item).isTop() ? rc : new AndConcept(rc,
						(Concept) item);
			}
		}
		return rc;
	}

	public static String[] getConstants() {
		if (oldSize != listOfConstantsInTbox.size()
				|| listOfConstantsArray == null) {
			oldSize = listOfConstantsInTbox.size();
			listOfConstantsArray = new String[oldSize];
			listOfConstantsArray = listOfConstantsInTbox
					.toArray(listOfConstantsArray);
		}
		return listOfConstantsArray.clone();
	}

}
